<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Lean projects</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  
<h1 id="lean-projects" class="markdown-heading">Lean projects <a class="hover-link" href="#lean-projects">#</a></h1>
<p>Every non-trivial piece of Lean code needs to live inside a <em>Lean project</em>
(sometimes also called Lean package).
This means a folder containing in particular a git repository and a file
<code>leanpkg.toml</code> that gathers information about dependencies of the
project, including for instance the version of Lean that should be used.</p>
<p>Managing all this is done by a little python program called <code>leanproject</code>.
This page describes the basic use of this tool, and should be sufficient
for everyday use.
If this is not enough for your purposes, you can read the
full <a href="../leanproject.html">leanproject documentation</a>.
If you are really curious, you can also read
<a href="../toolchain.html">how pieces fit together</a>.</p>
<p>There is a <a href="https://www.youtube.com/watch?v=y3GsHIe4wZ4">video walkthrough</a> of these instructions on YouTube.</p>
<h2 id="working-on-an-existing-project" class="markdown-heading">Working on an existing project <a class="hover-link" href="#working-on-an-existing-project">#</a></h2>
<p>Suppose you want to work on an existing project. As example, we will take
<a href="https://github.com/leanprover-community/tutorials">the tutorial project</a>.
Open a terminal.</p>
<ul>
<li>
<p>If you have not logged in since you installed Lean and mathlib, then
you may need to first type <code>source ~/.profile</code> or
<code>source ~/.bash_profile</code> depending on your OS.</p>
</li>
<li>
<p>Go the the directory where you would like this package to live.</p>
</li>
<li>
<p>Run <code>leanproject get tutorials</code>.</p>
</li>
<li>
<p>Launch VS Code, either through your application menu or by typing
<code>code tutorials</code>. (MacOS users need to take a one-off
<a href="https://code.visualstudio.com/docs/setup/mac#_launching-from-the-command-line">extra step</a>
to be able to launch VS Code from the command line.)</p>
</li>
<li>
<p>If you launched VS Code from a menu, on the main screen, or in the File menu,
click &quot;Open folder&quot; (just &quot;Open&quot; on a Mac), and choose the folder
<code>tutorials</code> (<em>not</em> one of its subfolders).</p>
</li>
<li>
<p>Using the file explorer on the left-hand side, explore everything you
want in <code>tutorials/src</code>.
See the <a href="https://github.com/leanprover-community/tutorials/blob/master/README.md">tutorials instructions</a>
for advice about how to do the exercises in this project.</p>
</li>
</ul>
<h2 id="creating-a-lean-project" class="markdown-heading">Creating a Lean project <a class="hover-link" href="#creating-a-lean-project">#</a></h2>
<p>We will now create a new project depending on mathlib. The following
commands should be typed in a terminal.</p>
<ul>
<li>
<p>Go to a folder where you want to create a project in a subfolder
<code>my_project</code>, and type <code>leanproject new my_project</code>. If you get an
error message saying <code>leanproject</code> is an unknown command and
you have not logged in since you installed Lean and mathlib, then
you may need to first type <code>source ~/.profile</code> or <code>source ~/.bash_profile</code>.</p>
</li>
<li>
<p>Launch VS Code, either through your application menu or by typing
<code>code my_project</code>.</p>
</li>
<li>
<p>If you launched VS Code through a menu: on the main screen, or in the
File menu, click &quot;Open folder&quot; (on a Mac, just &quot;Open&quot;), and
choose the folder <code>my_project</code> (<em>not</em> one of its subfolders).</p>
</li>
<li>
<p>Your Lean code should now be put inside files with extension <code>.lean</code>
living in <code>my_project/src/</code> or a subfolder thereof. In the file explorer
on the left-hand side of VS Code, you can right-click on <code>src</code>, choose
<code>New file</code>, and type a filename to create a file there.</p>
</li>
</ul>
<p>If you want to make sure everything is working, you can start by
creating, say <code>my_project/src/test.lean</code> containing:</p>
<pre><code class="language-lean">import topology.basic

#check topological_space
</code></pre>
<p>When the cursor is on the last line, the right hand part of VS Code
should display a &quot;Lean Goal&quot; area saying:
<code>topological_space : Type u_1 → Type u_1</code></p>
<p>If, for some reason, you happen to lose the &quot;Lean Goal&quot; area, you
can get it back with <kbd>Ctrl</kbd>-<kbd>Shift</kbd>-<kbd>Enter</kbd>
(<kbd>Cmd</kbd>-<kbd>Shift</kbd>-<kbd>Enter</kbd> on MacOS).
Also, you can get the Lean documentation inside VS Code using
<kbd>Ctrl</kbd>-<kbd>Shift</kbd>-<kbd>p</kbd>
(<kbd>Cmd</kbd>-<kbd>Shift</kbd>-<kbd>p</kbd> on MacOS) and then,
inside the text field that appears, type &quot;lean doc&quot; and hit <kbd>Enter</kbd>.
Then click &quot;Theorem Proving in Lean&quot; and enjoy.</p>
<h2 id="contributing-to-mathlib" class="markdown-heading">Contributing to mathlib <a class="hover-link" href="#contributing-to-mathlib">#</a></h2>
<p>See <a href="https://leanprover-community.github.io/contribute/index.html">How to contribute to mathlib</a>.</p>

  </div>
</div>

  <nav class="footer navbar navbar-expand-lg navbar-light bg-light justify-content-end">
  <ul class="nav">
    <li class="nav-item">
      <a class="nav-link active" href="https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/install/project.md">Suggest edits to this page on GitHub</a>
    </li>
  </ul>
</nav>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>